%!TEX root = forallxyyc.tex
\part{Metateoria}%\part{Metatheory}
\label{ch.normalform}
\addtocontents{toc}{\protect\mbox{}\protect\hrulefill\par}

%\chapter[Normal forms]{Normal forms and expressive completeness}
\chapter[Formas normais]{Formas normais e completude expressiva}


%\section{Disjunctive Normal Form}\label{s:DNFDefined}
\section{Forma Normal Disjuntiva}\label{s:DNFDefined}

%Sometimes it is useful to consider sentences of a particularly simple form. For instance, we might consider sentences in which $\enot$ only attaches to atomic sentences, or those which are combinations of atomic sentences and negated atomic sentences using only $\eand$.  A relatively general but still simple form is that where a sentence is a disjunction of conjunctions of atomic or negated atomic sentences.  When such a sentence is constructed, we start with atomic sentences, then (perhaps) attach negations, then (perhaps) combine using $\eand$, and finally (perhaps) combine using~$\eor$. 
%
Às vezes é útil considerar sentenças de uma forma particularmente simples. Por exemplo, podemos considerar sentenças em que $\enot$ apenas se liga a fórmulas atômicas, ou aquelas que são combinações de fórmulas atômicas e fórmulas atômicas negadas usando apenas o $\eand$. Uma forma relativamente geral, mas ainda assim simples, é aquela em que uma sentença é a disjunção de conjunções de fórmulas atômicas ou fórmulas atômicas negadas. Quando uma tal sentença é construída, nós começamos com sentenças atômicas, então (talvez) adicionamos negações, então (talvez) combinamos com $\eand$, e finalmente (talvez) combinamos usando~~$\eor$.

%Let's say that a sentence is in \define{disjunctive normal form} \emph{iff} it meets all of the following conditions:
Vamos dizer que uma sentença está na \define{forma normal disjuntiva} \emph{sse} ela cumpre todas as seguintes condições:
	\begin{earg}
		%\item[(\textsc{dnf1})] No connectives occur in the sentence other than negations, conjunctions and disjunctions;
		%\item[(\textsc{dnf2})] Every occurrence of negation has minimal scope (i.e.\ any `$\enot$' is immediately followed by an atomic sentence);
		%\item[(\textsc{dnf3})] No disjunction occurs within the scope of any conjunction.
		%
		\item[(\textsc{dnf1})] Nenhum conectivo ocorre na sentença além de negações, conjunções e disjunções;
		\item[(\textsc{dnf2})] Toda ocorrência da negação tem um escopo mínimo (i.e.\ qualquer `$\enot$' é imediatamente seguido de uma fórmula atômica);
		\item[(\textsc{dnf3})] Nenhuma disjunção ocorre dentro do escopo de qualquer conjunção.
	\end{earg}
\newglossaryentry{disjunctive normal form}{
  name = disjunctive normal form (DNF),
  text = disjunctive normal form,
  description = {a sentence which is a disjunction of conjunctions of atomic sentences or negated atomic sentences}
}
%So, here are are some sentences in disjunctive normal form:
Então, aqui estão algumas sentenças na forma normal disjuntiva:
\begin{align*}
  & A \\
  & (A \eand \lnot B \eand C)\\
  & (A \eand B) \eor (A \eand \enot B)\\
  & (A \eand B) \eor (A \eand  B \eand C \eand \enot D \eand \enot E)\\
  & A \eor (C \eand \enot P_{234} \eand P_{233} \eand Q) \eor \enot B
\end{align*}
%Note that we have here broken one of the maxims of this book and \emph{temporarily} allowed ourselves to employ the relaxed bracketing-conventions that allow conjunctions and disjunctions to be of arbitrary length. These conventions make it easier to see when a sentence is in disjunctive normal form. We will continue to help ourselves to these relaxed conventions, without further comment.
Note que nós quebramos aqui uma das máximas deste livro e \emph{temporariamente} nos permitimos a empregar as convenções relaxadas de parênteses que permitem que conjunções e disjunções tenham um tamanho arbitrário. Essas convenções farão fazem fácil ver quando uma sentença está na forma normal disjuntiva. Continuaremos tolerando essas convenções relaxadas, sem mais comentários.

%To further illustrate the idea of disjunctive normal form, we will introduce some more notation. We write `$\pm\meta{A}$' to indicate that $\meta{A}$ is an atomic sentence which may or may not be prefaced with an occurrence of negation. Then a sentence in disjunctive normal form has the following shape:
Para ilustrar melhor a ideia de forma normal disjuntiva, introduziremos mais algumas notações. Esrevemos `$\pm\meta{A}$' para indicar que $\meta{A}$ é uma sentença atômica que pode ou não estar precedida por uma ocorrência de negação. Então, uma sentença na forma normal disjuntiva tem a seguinte forma:
	$$(\pm \meta{A}_1 \land \ldots \land \pm \meta{A}_i) \lor (\pm \meta{A}_{i+1} \land \ldots \land \pm\meta{A}_j) \lor \ldots \lor (\pm\meta{A}_{m+1} \land \ldots \land \pm \meta{A}_n)$$
%We now know what it is for a sentence to be in disjunctive normal form. The result that we are aiming at is:
Agora, sabemos o que significa uma sentença estar na forma normal disjuntiva. O resultado que estamos procurando é:
	%\factoidbox{\label{thm:dnf}\textbf{Disjunctive Normal Form Theorem.} For any sentence, there is a logically equivalent sentence in disjunctive normal form.
	\factoidbox{\label{thm:dnf}\textbf{Teorema da Forma Normal Disjuntiva.} Para qualquer sentença, há uma sentença na forma normal disjuntiva logicamente equivalente.
	}
%Henceforth, we will abbreviate `Disjunctive Normal Form' by `DNF'. 
Daqui em diante, abreviaremos `Forma Normal Disjuntiva' por `FND'.

%\section{Proof of DNF Theorem via truth tables}
\section{Prova do teorema da FND via tabelas-verdade}
\label{s:DNFTruthTable}

%Our first proof of the DNF Theorem employs truth tables. We will first illustrate the technique for finding an equivalent sentence in DNF, and then turn this illustration into a rigorous proof. 
Nossa primeira prova do teorema da FND emprega tabelas-verdade. Primeiro, ilustraremos a técnica para encontrar uma sentença equivalente na FND, e então tornaremos esta ilustração em uma prova rigorosa.

%Let's suppose we have some sentence, $\meta{S}$, which contains three atomic sentences, `$A$', `$B$' and `$C$'. The very first thing to do is fill out a complete truth table for $\meta{S}$. Maybe we end up with this:
Suponhamos que temos alguma sentença, $\meta{S}$, que contém três sentenças atômicas,  `$A$', `$B$' e `$C$'. A primeira coisa a se fazer é completar uma tabela verdade para $\meta{S}$. Talvez nós terminemos com isso:
\begin{center}
\begin{tabular}{c c c | c}
$A$ & $B$ & $C$ & $\meta{S}$\\
\hline
 T & T & T & T \\
 T & T & F & F \\
 T & F & T & T \\
 T & F & F & F \\
 F & T & T & F \\
 F & T & F & F \\
 F & F & T & T \\
 F & F & F & T
\end{tabular}
\end{center}
%Now, consider a sentence, whose only connectives are negations and conjunctions, where no connective occurs within the scope of any negation, e.g.:
%	$$A \eand \enot B \eand C$$
%This sentence is true when, and only when, `$A$' is true, `$B$' is false and `$C$' is true. Similarly, the sentence:
%	$$\enot A \eand \enot B \eand C$$
%this is true when, and only when, `$A$' is false, `$B$' is false and `$C$' is true. 
%
%A disjunction is true when, and only when, at least one of the disjuncts is true. So if we write down a disjunction of sentences of the above form, perhaps
%	$$(A \eand \enot B \eand C) \eor (\enot A \eand \enot B \eand C)$$
%then it will be true on exactly \emph{two} lines of the truth table which describes all possible valuations of `$A$', `$B$' and `$C$'. 
%
%As it happens, $\meta{S}$ is true on four lines of its truth table, namely lines 1, 3, 7 and 8. Corresponding to each of those lines, we will write down four sentences, whose only connectives are negations and conjunctions, where every negation has minimal scope:
Por ocasião, $\meta{S}$ é verdadeiro em quatro linhas de sua tabela verdade, a saber, linhas 1, 3, 7 e 8. Correspondendo a cada uma dessas linhas, escreveremos quatro sentenças, cujos únicos conectivos são negações e conjunções, onde cada negação tem escopo mínimo:
	\begin{earg}
		%\item  `$A \eand B \eand C$'\hfill which is true on line 1 (and only then)
		%\item `$A \eand \enot B \eand C$' \hfill which is true on line 3 (and only then)
		%\item `$\enot A \eand \enot B \eand C$' \hfill which is true on line 7 (and only then)
		%\item `$\enot A \eand \enot B \eand \enot C$' \hfill which is true on line 8 (and only then)
		%
		\item  `$A \eand B \eand C$'\hfill que é verdadeiro na linha 1 (e apenas lá)
		\item `$A \eand \enot B \eand C$' \hfill que é verdadeiro na linha 3 (and only then)
		\item `$\enot A \eand \enot B \eand C$' \hfill que é verdadeiro na linha 7 (e apenas lá)
		\item `$\enot A \eand \enot B \eand \enot C$' \hfill que é verdadeiro na linha 8 (e apenas lá)
	\end{earg}
%We now combine all of these conjunctions using~$\eor$, like so:
Agora, combinamos todas essas conjunções usando~$\eor$, assim:
$$(A \eand B \eand C) \eor (A \eand \enot B \eand C) \eor (\enot A \eand \enot B \eand C) \eor (\enot A \eand \enot B \eand \enot C)$$
%This gives us a sentence in DNF which is true on exactly those lines where one of the disjuncts is true, i.e.\ it is true on (and only on) lines 1, 3, 7, and 8. So this sentence has exactly the same truth table as $\meta{S}$. So we have a sentence in DNF that is logically equivalent to $\meta{S}$, which is exactly what we wanted!
%
Isso nos dá uma sentença na FND que é verdadeira exatamente nessas linhas onde um dos disjuntos é verdadeiro, i.e.\ ela é verdadeira nas (e apenas nas) linhas 1, 3, 7 e 8. Então, essa sentença tem exatamente a mesma tabela verdade que $\meta{S}$. Então, temos uma sentença na FND que é logicamente equivalente a $\meta{S}$, que é exatamente o que queríamos!

%Now, the strategy that we just adopted did not depend on the specifics of $\meta{S}$; it is perfectly general. Consequently, we can use it to obtain a simple proof of the DNF Theorem.
Agora, a estratégia que adotamos não depende das especificidades de $\meta{S}$; ela é perfeitamente geral. Consequentemente, podemos usá-la para obter uma prova simples do teorema da FND.

%Pick any arbitrary sentence, $\meta{S}$, and let $\meta{A}_1, \ldots, \meta{A}_n$ be the atomic sentences that occur in $\meta{S}$. To obtain a sentence in DNF that is logically equivalent $\meta{S}$, we consider $\meta{S}$'s truth table. There are two cases to consider:
Escolha qualquer sentença arbitrária, $\meta{S}$, e seja $\meta{A}_1, \ldots, \meta{A}_n$ as sentenças atômicas que ocorrem em $\meta{S}$. Para obter uma sentença na FND que é logicamente equivalente a $\meta{S}$, consideramos a tabela verdade de $\meta{S}$. Aqui estão dois casos a serem considerados:
	\begin{enumerate}
		%\item \emph{$\meta{S}$ is false on every line of its truth table.} Then, $\meta{S}$ is a contradiction. In that case, the contradiction $(\meta{A}_1 \eand \enot \meta{A}_1)$ is in DNF and logically equivalent to~$\meta{S}$. 
		\item \emph{$\meta{S}$ é falso em todas as linhas de sua tabela verdade.} Então, $\meta{S}$ é uma contradição. Neste caso, a contradição $(\meta{A}_1 \eand \enot \meta{A}_1)$ está na FND e é logicamente equivalente a ~$\meta{S}$. 
	
		%\item \emph{$\meta{S}$ is true on at least one line of its truth table.}
		%For each line $i$ of the truth table, let $\meta{B}_i$ be a conjunction of the form 
		\item \emph{$\meta{S}$ é verdadeiro em pelo uma linha de sua tabela verdade.}
		Para cada linha $i$ da tabela verdade, seja $\meta{B}_i$ uma conjunção da forma
		$$(\pm\meta{A}_1 \land \ldots \land \pm\meta{A}_n)$$
		%where the following rules determine whether or not to include a negation in front of each atomic sentence:
		onde as seguintes regras determinam se deve-se ou não incluir uma negação na frente de cada sentença atômica:
			%\begin{align*}
			%	\meta{A}_m\text{ is a conjunct of }\meta{B}_i&\emph{ iff }\meta{A}_m\text{ is true on line }i\\
			%	\enot\meta{A}_m\text{ is a conjunct of }\meta{B}_i&\emph{ iff }\meta{A}_m\text{ is false on line }i
			%\end{align*}
			%
			\begin{align*}
				\meta{A}_m\text{ é um conjunto [\textit{conjunct}] de }\meta{B}_i&\emph{ iff }\meta{A}_m\text{ é verdadeiro na linha }i\\
				\enot\meta{A}_m\text{ é um \textit{conjunto} de  }\meta{B}_i&\emph{ iff }\meta{A}_m\text{ é falso na linha }i
			\end{align*}
		%Given these rules, $\meta{B_i}$ is true on (and only on) line $i$ of the truth table which considers all possible valuations of $\meta{A}_1, \ldots, \meta{A}_n$ (i.e.\ $\meta{S}$'s truth table). 
		Dadas estas regras, $\meta{B_i}$ é verdadeiro na (e apenas na) linha $i$ da tabela verdade que considera todas as possíveis valorações de $\meta{A}_1, \ldots, \meta{A}_n$ (i.e., a tabela verdade de $\meta{S}$). 
		
		%Next, let $i_1$, $i_2$, \dots, $i_m$ be the numbers of the lines of the truth table where $\meta{S}$ is \emph{true}. Now let $\meta{D}$ be the sentence:
		Em seguida, sejam $i_1$, $i_2$, \dots, $i_m$ os números de linhas da tabela verdade em que $\meta{S}$ é \emph{verdadeiro}. Agora, seja $\meta{D}$ a sentença:
		$$\meta{B}_{i_1} \eor \meta{B}_{i_2} \eor \ldots \eor \meta{B}_{i_m}$$
		%Since $\meta{S}$ is true on at least one line of its truth table, $\meta{D}$ is indeed well-defined; and in the limiting case where $\meta{S}$ is true on exactly one line of its truth table, $\meta{D}$ is just $\meta{B}_{i_1}$, for some $i_1$.
		%
		
		Uma vez que $\meta{S}$ é verdadeira em pelo menos uma linha de sua tabela verdade, $\meta{D}$ é de fato bem-definida; e no caso limitante em que $\meta{S}$ é verdadeira em exatamente uma linha de sua tabela verdade, $\meta{D}$ é apenas $\meta{B}_{i_1}$, para algum $i_1$.
		
		%By construction, $\meta{D}$ is in DNF. Moreover, by construction, for each line~$i$ of the truth table: $\meta{S}$ is true on line $i$ of the truth table \emph{iff} one of $\meta{D}$'s disjuncts (namely, $\meta{B_i}$) is true on, and only on, line $i$. Hence $\meta{S}$ and $\meta{D}$ have the same truth table, and so are logically equivalent.
		Por construção, $\meta{D}$ está na FND. Além do mais, por construção, para cada linha~$i$ da tabela verdade: $\meta{S}$ é verdadeiro na linha $i$ da tabela verdade \emph{sse} um dos disjuntos de $\meta{D}$ (a saber, $\meta{B_i}$) é verdadeiro na, e apenas na, linha $i$. Consequentemente, $\meta{S}$ e $\meta{D}$ têm o mesmo valor verdade, e então são logicamente equivalentes.
	\end{enumerate}
	%These two cases are exhaustive and, either way, we have a sentence in DNF that is logically equivalent to $\meta{S}$.
	Esses dois casos são exaustivos e, de qualquer forma, teremos uma sentença na FND que é logicamente equivalente a $\meta{S}$.

%So we have proved the DNF Theorem. Before we say any more, though, we should immediately flag that we are hereby returning to the austere definition of a (TFL) sentence, according to which we can assume that any conjunction has exactly two conjuncts, and any disjunction has exactly two disjuncts.
Então, nós provamos o Teorema da DNF. Antes de dizermos mais, porém, devemos sinalizar imediatamente que estamos retornando à definição austera de uma sentença (LVF), segundo a qual podemos assumir que qualquer conjunção tem exatamente dois conjuntos [\emph{conjuncts}] e qualquer disjunção possui exatamente dois disjuntos.


\section{Forma Normal Conjuntiva}%\section{Conjunctive Normal Form}
\label{s:CNF}

%So far in this chapter, we have discussed \emph{disjunctive} normal form. It may not come as a surprise to hear that there is also such a thing as \emph{conjunctive normal form} (CNF).
Até este capítulo, discutimos formas normais \emph{disjuntivas}. Não seria uma surpresa ouvir dizer que há também uma coisa como uma \emph{forma normal conjuntiva} (FNC).

%The definition of CNF is exactly analogous to the definition of DNF. So, a sentence is in CNF \emph{iff} it meets all of the following conditions:
A definição de FNC é exatamente análoga à definição de FND. Então, uma sentença está na FNC \emph{sse} ela cumpre todas as seguitnes condições:
	\begin{earg}
		%\item[(\textsc{cnf1})] No connectives occur in the sentence other than negations, conjunctions and disjunctions;
		%\item[(\textsc{cnf2})] Every occurrence of negation has minimal scope;
		%\item[(\textsc{cnf3})] No conjunction occurs within the scope of any disjunction. 
		%
		\item[(\textsc{cnf1})] Nenhum conectivo ocorre na sentença além de negações, conjunções e disjunções;
		\item[(\textsc{cnf2})] Toda ocorrência da negação tem um escopo mínimo;
		\item[(\textsc{cnf3})] Nenhuma conjunção ocorre dentro do escopo de qualquer disjunção. 
	\end{earg}
\newglossaryentry{conjunctive normal form}{
  name = conjunctive normal form (DNF),
  text = conjunctive normal form,
  description = {a sentence which is a conjunction of disjunctions of atomic sentences or negated atomic sentences}
}
%Generally, then, a sentence in CNF looks like this
De modo geral, então, uma sentença na FNC se parece com isso:
	$$(\pm \meta{A}_1 \lor \ldots \lor \pm \meta{A}_i) \land (\pm \meta{A}_{i+1} \lor \ldots \lor \pm\meta{A}_j) \land \ldots \land (\pm\meta{A}_{m+1} \lor\ldots \lor \pm \meta{A}_n)$$
%where each $\meta{A}_k$ is an atomic sentence.
onde cada $\meta{A}_k$ é uma sentença atômica.

%We can now prove another normal form theorem:
Podemos agora provar outro teorema da forma normal:
	%\factoidbox{\label{thm:cnf}\textbf{Conjunctive Normal Form Theorem.} For any sentence, there is a logically equivalent sentence in conjunctive normal form.}
	\factoidbox{\label{thm:cnf}\textbf{Teorema da Forma Normal Conjuntiva.} Para qualquer sentença, há uma sentença na forma normal conjuntiva equivalente.}

        
	%Given a TFL sentence, $\meta{S}$, we begin by writing down the complete truth table for $\meta{S}$.
	Dada uma sentença da LVF, $\meta{S}$, começamos escrevendo a tabela verdade para $\meta{S}$.
	
	%If $\meta{S}$ is \emph{true} on every line of the truth table, then $\meta{S}$ and $(\meta{A}_1 \eor \enot \meta{A}_1)$ are logically equivalent.
	Se $\meta{S}$ é \emph{verdadeiro} em toda linha da tabela verdade, então $\meta{S}$ e $(\meta{A}_1 \eor \enot \meta{A}_1)$ são logicamente equivalentes
	
	%If $\meta{S}$ is \emph{false} on at least one line of the truth table then, for every line on the truth table where $\meta{S}$ is false, write down a disjunction $(\pm\meta{A}_1 \eor \ldots \eor \pm\meta{A}_n)$ which is \emph{false} on (and only on) that line. Let $\meta{C}$ be the conjunction of all of these disjuncts; by construction, $\meta{C}$ is in CNF and $\meta{S}$ and $\meta{C}$ are logically equivalent.
	Se $\meta{S}$ é \emph{falsa} em pelo menos uma linha da tabela verdade, então, para toda linha da tabela verdade onde $\meta{S}$ é falso, escreva uma disjunção $(\pm\meta{A}_1 \eor \ldots \eor \pm\meta{A}_n)$ que é \emph{falsa} nessa (e apenas nessa) linha. Seja $\meta{C}$ a conjunção de todas esses três disjuntos; por construção, $\meta{C}$ está na FNC e $\meta{S}$ e $\meta{C}$ são logicamente equivalentes.

\practiceproblems
\problempart
\label{pr.DNF}
Considere as seguintes sentenças: %Consider the following sentences:
	\begin{earg}
		\item $(A \eif \enot B)$
		\item $\enot (A \eiff B)$
		\item $(\enot A \eor \enot (A \eand B))$
		\item $(\enot (A \eif B ) \eand (A \eif C))$
		\item $(\enot (A \eor B) \eiff ((\enot C \eand \enot A) \eif \enot B))$
		\item $((\enot (A \eand \enot B) \eif C) \eand \enot (A \eand D))$
	\end{earg}
       % For each sentence, find a logically equivalent sentence in DNF and one in CNF.
       Para cada sentença, encontre uma sentença logicamente equivalente na FND e uma na FNC.
        
\section{A adequação expressiva da LVF}%\section{The expressive adequacy of TFL}

%Of our connectives, $\enot$ attaches to a single sentences, and the others all combine exactly two sentences. We may also introduce the idea of an $n$-place connective. For example, we could consider a three-place connective, `$\heartsuit$', and stipulate that it is to have the following characteristic truth table:
Dos nossos conectivos, o $\enot$ se liga a sentenças simples, e todos os outros se combinam exatamente com duas sentenças. Poderíamos também introduzir a ideia de um conectivo $n$-ário. Por exemplo, poderíamos considerar um conectivo ternário, `$\heartsuit$', e estipular que ele deve ter a seguinte tabela verdade característica:
\begin{center}
\begin{tabular}{c c c | c}
$A$ & $B$ & $C$ & $\heartsuit(A,B,C)$\\
\hline
 T & T & T & F \\
 T & T & F & T \\
 T & F & T & T \\
 T & F & F & F \\
 F & T & T & F \\
 F & T & F & T \\
 F & F & T & F \\
 F & F & F & F
\end{tabular}
\end{center}
%Probably this new connective would not correspond with any natural English expression (at least not in the way that `$\eand$' corresponds with `and'). But a question arises: if we wanted to employ a connective with this characteristic truth table, must we add a \emph{new} connective to TFL? Or can we get by with the connectives we \emph{already have}?
%
Provavelmente este novo conectivo não corresponderia a qualquer sentença natural da língua portuguesa (pelo menos não da forma com que `$\eand$' corresponde a `e'). Mas surge uma questão: se quiséssemos empregar um conectivo com esta tabela verdade característica, deveríamos adicionar um \emph{novo} conectivo à LVF? Ou poderíamos conseguir isso com os conectivos que nós \emph{já temos}?

%Let us make this question more precise. Say that some connectives are \define{jointly expressively adequate} \emph{iff}, for any possible truth table, there is a sentence containing only those connectives with that truth table.
Vamos tornar esta questão mais precisa. Digamos que alguns conectivos são \define{conjuntamente expressivamente adequados} \emph{sse}, para qualquer tabela verdade possível, há uma sentença contendo apenas aqueles conectivos com aquela tabela verdade.

\newglossaryentry{expressively adequate}{
  name = {expressive adequacy},
  text = {expressively adequate},
  description = {property of a collection of connectives which holds iff every possible truth table is the truth table of a sentence involving only those connectives}}

%The general point is, when we are armed with some jointly expressively adequate connectives, no characteristic truth table lies beyond our grasp. And in fact, we are in luck.
%
O ponto geral é que, quando estamos armados com alguns conectivos expressivamente adequados em conjunto, nenhuma tabela verdade característica está além de nosso alcance. E, de fato, estamos com sorte.
	%\factoidbox{\label{thm:ExpressiveAdequacy}\textbf{Expressive Adequacy Theorem.}
	\factoidbox{\label{thm:ExpressiveAdequacy}\textbf{Teorema da adequação expressiva.}
%The connectives of TFL are jointly expressively adequate. Indeed, the following pairs of connectives are jointly expressively adequate:
Os conectivos da LVF são expressivamente adequados em conjunto. De fato, os seguintes pares de conectivos são expressivamente adequados em conjunto:
\begin{earg}
\item\label{expressive:eor} `$\enot$' e `$\eor$'% and `$\eor$'
\item\label{expressive:eand} `$\enot$' e `$\eand$'% and `$\eand$'
\item\label{expressive:eif} `$\enot$' e `$\eif$' % and `$\eif$'
\end{earg}}

%Given any truth table, we can use the method of proving the DNF Theorem (or the CNF Theorem) via truth tables, to write down a scheme which has the same truth table. For example, employing the truth table method for proving the DNF Theorem, we find that the following scheme has the same characteristic truth table as $\heartsuit(A,B,C)$, above:
Dada qualquer tabela verdade, podemos usar o método de provar o teorema da FND (ou o da FNC) via tabelas verdade para escrever um esquema que tem a mesma tabela verdade. Por exeplo, empregando o método verdade para provar o teorema da FND, descobrimos que os seguintes esquemas têm as mesmas tabelas características que $\heartsuit(A,B,C)$ acima:
		$$(A \eand B \eand \enot C) \eor (A \eand \enot B \eand C) \eor (\enot A \eand B \eand \enot C)$$			
%It follows that the connectives of TFL are jointly expressively adequate. We now prove each of the subsidiary results.
Segue-se que os conectivos da LVF são expressivamente adequados em conjunto.
	
%\emph{Subsidiary Result \ref{expressive:eor}: expressive adequacy of `$\enot$' and `$\eor$'.} Observe that the scheme that we generate, using the truth table method of proving the DNF Theorem, will only contain the connectives `$\enot$', `$\eand$' and `$\eor$'. So it suffices to show that there is an equivalent scheme which contains only `$\enot$' and `$\eor$'. To show do this, we simply consider that
\emph{Resultado Subsidiário \ref{expressive:eor}: adequação expressiva de `$\enot$' and `$\eor$'.} Observe que o esquema que geramos, usando o método de tabela verdade de provar o teorema da FND, conterá apenas os conectivos `$\enot$', `$\eand$' e `$\eor$'. Então, ele é suficiente para mostrar que há um esquema equivalente que contém apenas `$\enot$' e `$\eor$'. Para mostrar isso, simplesmente consideramos que 
	%	\begin{align*}
	%	(\meta{A} \eand \meta{B}) & \text{\quad and \quad} \enot(\enot \meta{A} \eor\enot \meta{B})
	%	\end{align*}
			\begin{align*}
		(\meta{A} \eand \meta{B}) & \text{\quad e \quad} \enot(\enot \meta{A} \eor\enot \meta{B})
		\end{align*}
		são logicamente equivalentes.%are logically equivalent.

%\emph{Subsidiary Result \ref{expressive:eand}: expressive adequacy of `$\enot$' and `$\eand$'.} Exactly as in Subsidiary Result~\ref{expressive:eor}, making use of the fact that
\emph{Resultado Subsidiário \ref{expressive:eand}: adequação expressiva de `$\enot$' and `$\eand$'.} Exatamente como no Resultado Subsidiário~\ref{expressive:eor}, faz-se o uso do fato de que 
		%\begin{align*}
		%(\meta{A} \eor \meta{B}) & \text{\quad and \quad}\enot(\enot \meta{A} \eand\enot \meta{B})
		%\end{align*}
		\begin{align*}
		(\meta{A} \eor \meta{B}) & \text{\quad e \quad}\enot(\enot \meta{A} \eand\enot \meta{B})
		\end{align*}
são logicamente equivalentes..

%\emph{Subsidiary Result \ref{expressive:eif}: expressive adequacy of `$\enot$' and `$\eif$'.} Exactly as in Subsidiary Result~\ref{expressive:eor}, making use of these equivalences instead:
\emph{Resultado Subsidiário \ref{expressive:eif}: adequação expressiva de `$\enot$' and `$\eif$'.} Exatamente como no Resultado Subsidiário~\ref{expressive:eor}, faz-se o uso dessas equivalências:
		%\begin{align*}
		%(\meta{A} \eor \meta{B}) &\text{\quad and \quad} (\enot \meta{A} \eif \meta{B})\\
		%(\meta{A} \eand \meta{B}) &\text{\quad and \quad} \enot(\meta{A} \eif \enot\meta{B})
		%\end{align*}
		\begin{align*}
		(\meta{A} \eor \meta{B}) &\text{\quad e \quad} (\enot \meta{A} \eif \meta{B})\\
		(\meta{A} \eand \meta{B}) &\text{\quad e \quad} \enot(\meta{A} \eif \enot\meta{B})
		\end{align*}
%Alternatively, we could simply rely upon one of the other two subsidiary results, and (repeatedly) invoke only one of these two equivalences.
Alternativamente, poderíamos simplesmente confiar em um dos outros dois resultados subsidiários e (repetidamente) invocar apenas uma dessas duas equivalências. 

%In short, there is never any \emph{need} to add new connectives to TFL. Indeed, there is already some redundancy among the connectives we have: we could have made do with just two connectives, if we had been feeling really austere.
Em suma, nunca há qualquer \emph{necessidade} de se adicionar conectivos à LVF. De fato, já há alguma redundância entre os conectivos que temos: poderíamos nos contentar com apenas dois conectivos, se estivéssemos nos sentindo realmente austeros.

%\section{Individually expressively adequate connectives}
\section{Conectivos individualmente expressivamente adequados}

%In fact, some two-place connectives are \emph{individually} expressively adequate. These connectives are not standardly included in TFL, since they are rather cumbersome to use. But their existence shows that, if we had wanted to, we could have defined a truth-functional language that was expressively adequate, which contained only a single primitive connective.
%
De fato, alguns conectivos binários são \emph{individualmente} expressivamente adequados. Estes conectivos não estão normalmente incluídos na LVF, uma vez que eles são bem complexos de se usar. Mas a existência deles mostra que, se quiséssemos, poderíamos definir uma linguagem vero-funcional que fosse expressivamente adequada que contivesse apenas um único operador primitivo.

%The first such connective we will consider is `$\uparrow$', which has the following characteristic truth table. 
O primeiro desses conectivos que consideraremos é `$\uparrow$', que tem a seguinte tabela verdade característica.
\begin{center}
\begin{tabular}{c c | c}
$\meta{A}$ & $\meta{B}$ & $\meta{A} \mathrel{\uparrow} \meta{B}$\\
\hline
 T & T & F \\
 T & F & T \\
 F & T & T  \\
 F & F & T
\end{tabular}
\end{center}
% This is often called `the Sheffer stroke', after Henry Sheffer, who used it to show how to reduce the number of logical connectives in Russell and Whitehead's \emph{Principia Mathematica}.\footnote{Sheffer, `A Set of Five Independent Postulates for Boolean Algebras, with application to logical constants,' (1913, \emph{Transactions of the American Mathematical Society} 14.4)} (In fact, Charles Sanders Peirce had anticipated Sheffer by about 30 years, but never published his results.)\footnote{See Peirce, `A Boolian Algebra with One Constant', which dates to c.1880; and Peirce's \emph{Collected Papers}, 4.264--5.} It is quite common, as well, to call it `nand', since its characteristic truth table is the negation of the truth table for `$\eand$'.
 Ele é frequente chamado de `\textit{Sheffer stroke}', depois de Henry Sheffer, quem o utilizou para mostrar como reduzir o número de conectivos lógicos no \emph{Principia Mathematica} de Russell e Whitehead.\footnote{Sheffer, `A Set of Five Independent Postulates for Boolean Algebras, with application to logical constants,' (1913, \emph{Transactions of the American Mathematical Society} 14.4)}
\factoidbox{\label{prop:upexpressive}`$\uparrow$' é expressivamente adequado sozinho.} (Na verdade, Charles Sanders Peirce antecipou Sheffer em cerca de 30 anos, mas nunca publicou seus resultados.)\footnote{Ver Peirce, `A Boolian Algebra with One Constant', que é datado de c.1880; e Peirce's \emph{Collected Papers}, 4.264--5.} É bem comum, também, chamá-lo de `nand', uma vez que sua tabela verdade característica é a negação da tabela verdad do `$\eand$'.

%The Expressive Adequacy Theorem tells us that `$\enot$' and `$\eor$' are jointly expressively adequate. So it suffices to show that, given any scheme which contains only those two connectives, we can rewrite it as a logically equivalent scheme which contains only `$\uparrow$'. As in the proof of the subsidiary cases of the Expressive Adequacy Theorem, then, we simply apply the following equivalences:
O Teorema da Adequação Expressiva nos diz que `$\enot$' e `$\eor$' são conjuntamente expressivamente adequados. Então, ele é suficiente para nos mostrar que, dado qualquer esquema que contenha apenas esses dois conectivos, podemos reescrevê-lo como um esquema logicamente equivalente que contém apenas `$\uparrow$'. Como na prova dos casos subsidiários do Teorema da Adequação Expressiva, então, nós simplesmente aplicamos as seguintes equivalências:
		%\begin{align*}
		%	\enot \meta{A} &\text{\quad and \quad} (\meta{A} \uparrow \meta{A})\\
		%	(\meta{A} \eor \meta{B}) & \text{\quad and \quad} ((\meta{A} \uparrow \meta{A}) \uparrow (\meta{B} \uparrow \meta{B}))
		%\end{align*}
		%
		\begin{align*}
			\enot \meta{A} &\text{\quad e \quad} (\meta{A} \uparrow \meta{A})\\
			(\meta{A} \eor \meta{B}) & \text{\quad e \quad} ((\meta{A} \uparrow \meta{A}) \uparrow (\meta{B} \uparrow \meta{B}))
		\end{align*}
%to the Subsidiary Result~\ref{expressive:eor}.
para o resultado subsidiário~\ref{expressive:eor}.

%Similarly, we can consider the connective `$\downarrow$':
De maneira similar, podemos considerar o conectivo `$\downarrow$':
\begin{center}
\begin{tabular}{c c | c}
$\meta{A}$ & $\meta{B}$ & $\meta{A} \mathrel{\downarrow} \meta{B}$\\
\hline
 T & T & F \\
 T & F & F  \\
 F & T & F  \\
 F & F & T
\end{tabular}
\end{center}
%This is sometimes called the `Peirce arrow' (Peirce himself called it `ampheck'). More often, though, it is called `nor', since its characteristic truth table is the negation of `$\eor$', that is, of `neither \dots{} nor \dots'.
Ele é às vezees chamado de `\textit{Peirce arrow}' (Peirce o chamou de \textit{ampheck}). Mais frequentemente, porém, ele é chamado de `nor', uma vez que sua tabela verdade característica é a negação de `$\eor$', ou seja, de `nem \dots{} nem \dots'.
	\factoidbox{
	%`$\downarrow$' is expressively adequate all by itself. }
	`$\downarrow$' é expressivamente adequado por si só. }

%As in the previous result for $\uparrow$, although invoking the equivalences:
Como no resultado anterior para $\uparrow$, porém, invocando as equivalências:
		%\begin{align*}
		%	\enot \meta{A} &\text{\quad and \quad} (\meta{A} \downarrow \meta{A})\\
		%	(\meta{A} \eand \meta{B}) & \text{\quad and \quad} ((\meta{A} \downarrow \meta{A}) \downarrow (\meta{B} \downarrow \meta{B}))
		%\end{align*}
		%
		\begin{align*}
			\enot \meta{A} &\text{\quad e \quad} (\meta{A} \downarrow \meta{A})\\
			(\meta{A} \eand \meta{B}) & \text{\quad e \quad} ((\meta{A} \downarrow \meta{A}) \downarrow (\meta{B} \downarrow \meta{B}))
		\end{align*}
%and Subsidiary Result~\ref{expressive:eand}.
e o resultado subsidiário~\ref{expressive:eand}.


%\section{Failures of expressive adequacy}
\section{Falhas de adequação expressiva}

%In fact, the \emph{only} two-place connectives which are individually expressively adequate are `$\uparrow$' and `$\downarrow$'. But how would we show this? More generally, how can we show that some connectives are \emph{not} jointly expressively adequate? 
De fato, os \emph{únicos} conectivos binários que são individualmente expressivamente adequados são `$\uparrow$' e `$\downarrow$'. Mas como mostraríamos isso? De maneira mais geral, como podemos mostrar que alguns conectivos \emph{não} são conjuntamente expressivamente adequados?
 
%The obvious thing to do is to try to find some truth table which we \emph{cannot} express, using just the given connectives. But there is a bit of an art to this.
A coisa óbvia a se fazer é tentar encontrar alguma tabela verdade que \emph{não podemos} expressar usando apenas os conectivos dados. Mas há um pouco de arte nisso.

%To make this concrete, let's consider the question of whether `$\eor$' is expressively adequate all by itself. After a little reflection, it should be clear that it is not. In particular, it should be clear that any scheme which only contains disjunctions cannot have the same truth table as negation, i.e.:
Para tornar isso concreto, vamos considerar a questão sobre se `$\eor$' é expressivamente adequado por si só. Depois de um pouco de reflexão, deve estar claro que ele não é. Em particular, deve estar claro que qualquer esquema que contenha apenas disjunções não pode ter a mesma tabela verdade que a negação, i.e.:
				\begin{center}
				\begin{tabular}{c | c}
				$\meta{A}$ & $\enot \meta{A}$\\
				\hline
				 T & F \\
				 F & T
				\end{tabular}
				\end{center}
%The intuitive reason, why this should be so, is simple: the top line of the desired truth table needs to have the value False; but the top line of any truth table for a scheme which \emph{only} contains $\eor$ will always be True. The same is true for $\eand$, $\eif$, and $\eiff$.
A razão intuitiva de por que isso deve ser assim é simples: as linhas do topo da tabela verdade desejada precisam ter o valor falso; mas a linha do topo de qualquer tabela para um esquema que contém \emph{apenas} $\eor$ sempre será verdadeiro. O mesmo é verdadeiro para $\eand$, $\eif$, e $\eiff$.
 	\factoidbox{
		%`$\eor$', `$\eand$', `$\eif$', and `$\eiff$' are not expressively adequate by themselves.}
		`$\eor$', `$\eand$', `$\eif$', e `$\eiff$' não são expressivamente adequados por si só.}

%In fact, the following is true:
Na verdade, o seguinte é verdadeiro:
        
%\factoidbox{The \emph{only} two-place connectives that are expressively adequate by themselves are `$\uparrow$' and `$\downarrow$'. }
\factoidbox{Os \emph{únicos} conectivos binários que são expressivamente adequados por si só são `$\uparrow$' e `$\downarrow$'. }

%This is of course harder to prove than for the primitive connectives. For instance, the ``exclusive or'' connective does not have a T in the first line of its characteristic truth table, and so the method used above no longer suffices to show that it cannot express all truth tables.  It is also harder to show that, e.g., `$\eiff$' and `$\enot$' \emph{together} are not expressively adequate.

Certamente, isso é mais difícil de se provar do que para conectivos primitivos. Por exemplo, o conectivo de ``disjunção exclusiva'' não tem um T na primeira linha de sua tabela verdade característica, então o método usado acima não é mais suficiente para mostrar que ele não pode expressar todas as tabelas verdades. Também é mais difícil mostrar que, e.g., `$\eiff$' e `$\enot$' \emph{juntos} não são expressivamente adequados.

%\chapter{Soundness}\label{ch:Soundness}
\chapter{Correção}\label{ch:Soundness}

%In this chapter we relate TFL's semantics to its natural deduction \emph{proof system} (as defined in Part~\ref{ch.NDTFL}). We will prove that the formal proof system is safe: you can only prove sentences from premises from which they actually follow.
Neste capítulo, relacionaremos a semântica da LVF ao seu \emph{sistema de prova} de dedução natural (conforme definido na parte~\ref{ch.NDTFL}). Provaremos que o sistema formal de prova é seguro: você pode provar sentenças apenas de premissas das quais elas se seguem.
%Intuitively, a formal proof system is sound iff it does not allow you to prove any invalid arguments. This is obviously a highly desirable property. It tells us that our proof system will never lead us astray. Indeed, if our proof system were not sound, then we would not be able to trust our proofs. The aim of this chapter is to prove that our proof system is sound.
%
Intuitivamente, um sistema formal de prova é correto [\textit{sound}] sse ele não nos permite provar qualquer argumento inválido. Isso obviamente é uma propriedade fortemente desejável. Ela nos diz que nossos sistema de prova jamais nos desviará. Na verdade, se nosso sistema de prova não fosse correto, então nós não poderíamos confiar em nossas provas. O objetivo deste capítulo é provar que nosso sistema de prova é correto. 

%Let's make the idea more precise. We'll abbreviate a list of sentences using the greek letter $\Gamma$ (`gamma'). A formal proof system is \define{sound} (relative to a given semantics) \emph{iff}, whenever there is a formal proof of $\meta{C}$ from assumptions among $\Gamma$, then $\Gamma$ genuinely entails $\meta{C}$ (given that semantics). Otherwise put, to prove that TFL's proof system is sound, we need to prove the following
%
Vamos fazer a ideia mais precisa. Abreviaremos uma lista de sentenças usando a letra grega $\Gamma$ (`gamma'). Um sistema formal de prova é \define{correto [\textit{sound}]} (relativo a uma dada semântica) \emph{sse}, sempre que houver uma prova de $\meta{C}$ a partir de assunções de $\Gamma$, então $\Gamma$ genuinamente acarreta [\textit{entails}] $\meta{C}$ (dada essa semântica). Posto de outra maneira, para provar que o sistema de prova da LVF é correto, precisamos provar o seguinte

%\begin{factoidboxe}\textbf{Soundness Theorem.} For any sentences $\Gamma$ and $\meta{C}$: if $\Gamma\proves\meta{C}$, then $\Gamma \entails\meta{C}$
\begin{factoidboxe}\textbf{Teorema da Correção.}
Para quaisquer sentenças $\Gamma$ e $\meta{C}$: se $\Gamma\proves\meta{C}$, então $\Gamma \entails\meta{C}$
\end{factoidboxe}

%To prove this, we will check each of the rules of TFL's proof system individually. We want to show that no application of those rules ever leads us astray. Since a proof just involves repeated application of those rules, this will show that no proof ever leads us astray. Or at least, that is the general idea.
Para provar isso, checaremos cada uma das regras do sistema de prova da LVF individualmente. Queremos mostrar que nenhuma aplicação dessas regras nos engana. Uma vez que uma prova apenas envolve aplicações repetidas dessas regras, isso mostrará que nenhuma prova nos engana. Ou, pelo menos, essa é a ideia geral.

%To begin with, we must make the idea of `leading us astray' more precise. Say that a line of a proof is \define{shiny} iff the assumptions on which that line depends tautologically entail the sentence on that line.\footnote{The word `shiny' is not standard among logicians.} To illustrate the idea, consider the following:
Para começar, precisamos tornar a ideia de `nos enganar' mais precisa. Digamos que uma linha de uma prova é \define{brilhante} sse as assunções das quais essa linha depende acarretam tautologicamente a sentença nessa linha.\footnote{A palavra `brilhante' não é padronizada entre os lógicos.} Para ilustrar a ideia, considere o seguinte:
	\begin{proof}
		\hypo{fgh}{F\eif(G\eand H)}
		\open
			\hypo{f}{F}
			\have{gh}{G \eand H}\ce{fgh,f}
			\have{g}{G}\ae{gh}
		\close
		\have{fg}{F \eif G}\ci{f-g}
	\end{proof}\noindent\noindent
%Line $1$ is shiny iff $F \eif (G \eand H) \entails F \eif (G \eand H)$. You should be easily convinced that line $1$ is, indeed, shiny! Similarly, line $4$ is shiny iff $F \eif (G \eand H), F \entails G$. Again, it is easy to check that line $4$ is shiny. As is every line in this TFL-proof. We want to show that this is no coincidence. That is, we want to prove:
A linha $1$ é brilhante sse $F \eif (G \eand H) \entails F \eif (G \eand H)$. Você deveria ser facilmente convencido de que a linha $1$ é de fato brilhante! De maneira similar, a linha $4$ é brlihante sse $F \eif (G \eand H), F \entails G$. Novamente, é fácil checar que a linha $4$ é brilhante. Assim como o é em toda linha nessa prova da LVF. Queremos mostrar que isso não é uma coincidência. Isto é, queremos provar:
	%\begin{factoidboxe}\textbf{Shininess Lemma.}
	%	Every line of every TFL-proof is shiny.
	%\end{factoidboxe}\noindent
	%
	\begin{factoidboxe}\textbf{Lema do Brilho.}
		Toda linha de toda prova da LVF é brilhante.
	\end{factoidboxe}\noindent
%Then we will know that we have never gone astray, on any line of a proof. Indeed, given the Shininess Lemma, it will be easy to prove the Soundness Theorem:
Então, saberemos que nunca seremos enganados, em qualquer linha de uma prova. De fato, dado o Lema do Brilho, será fácil provar o Teorema da Correção:

%\emph{Proof.} Suppose $\Gamma \proves \meta{C}$. Then there is a TFL-proof, with $\meta{C}$ appearing on its last line, whose only undischarged assumptions are among $\Gamma$. The Shininess Lemma tells us that every line on every TFL-proof is shiny. So this last line is shiny, i.e.\ $\Gamma \entails \meta{C}$. QED
%
\emph{Prova.} Suponha que $\Gamma \proves \meta{C}$. Então, há uma prova da LVF, com $\meta{C}$ aparecendo em sua última linha, cujas únicas assunções não eliminadas estão entre $\Gamma$. O Lema do Brilho nos diz que toda linha em uma prova da LVF é brilhante. Então, esta última linha é brilhante, i.e.\ $\Gamma \entails \meta{C}$. QED

%It remains to prove the Shininess Lemma. 
Ainda falta provar o Lema do Brilho.

%To do this, we observe that every line of any TFL-proof is obtained by applying some rule. So what we want to show is that no application of a rule of TFL's proof system will lead us astray. More precisely, say that a rule of inference is \define{rule-sound} \emph{iff} for all TFL-proofs, if we obtain a line on a TFL-proof by applying that rule, and every earlier line in the TFL-proof is shiny, then our new line is also shiny. What we need to show is that \emph{every} rule in TFL's proof system is rule-sound. 
Para fazer isso, observe que toda linha de qualquer prova da LVF é obtida ao se aplicar alguma regra. Então o que queremos mostrar é que nenhuma aplicação de uma regra do sistema de prova da LVF nos enganará. Mais precisamente, digamos que uma regra de inferência é \define{correta} [\textit{rule-sound}] \emph{sse} para todas as provas da LVF, se obtivermos uma linha em uma prova da LVF ao aplicar aquela regra, e todas as linhas anteriores na prova da LVF forem brilhantes, então nossa nova linha é também brilhante. O que precisamos mostrar é que \emph{todas} as regras no sistema de provas da LVF são corretas. 

%We will do this in the next section. But having demonstrated the rule-soundness of every rule, the Shininess Lemma will follow immediately:
Faremos isso na próxima seção. Mas, tendo demonstrado a correção de todas as regras, o Lema do Brilho seguirá imediatamente:


%\emph{Proof.} Fix any line, line $n$, on any TFL-proof. The sentence written on line $n$ must be obtained using a formal inference rule which is rule-sound. This is to say that, if every earlier line is shiny, then line $n$ itself is shiny. Hence, by strong induction on the length of TFL-proofs, every line of every TFL-proof is shiny. QED
\emph{Prova.} Fixe qualquer linha, linha $n$, em qualquer prova da LVF. A sentença escrita na linha $n$ deve ser obtida usando uma regra de inferência formal que é correta. Isso é dizer que, se toda linha anterior é brilhante, então a linha $n$ é ela mesma brilhante. Consequentemente, pelo teorema forte da indução no tamanho das provas da LVF, toda linha de toda prova da LVF é brilhante. QED.

%Note that this proof appeals to a principle of strong induction on the length of TFL-proofs. This is the first time we have seen that principle, and you should pause to confirm that it is, indeed, justified.
Note que esta prova apela a um princípio da indução forte no tamanho das provas da LVF. Esta é a primeira vez que nós vimos este princípio, e você deveria pausar para confirmar que ele é, de fato, justificado.

%It remains to show that every rule is rule-sound. This is not difficult, but it is time-consuming, since we need to check each rule individually, and TFL's proof system has plenty of rules! To speed up the process marginally, we will introduce a convenient abbreviation: `$\Delta_i$' (`delta') will abbreviate the assumptions (if any) on which line $i$ depends in our TFL-proof (context will indicate which TFL-proof we have in mind).
Resta mostrar que toda regra é correta. Isso não é difícil, mas é consumidor de tempo, uma vez que precisamos checar cada regra individualmente, e o sistema de prova da LVF tem várias regras! Para acelerar o processo marginalmente, introduziremos uma abreviação conveniente: `$\Delta_i$' (`delta') abreviará as assunções (se houver) em que a linha $i$ depende da nossa prova na LVF (o contexto indicará qual prova da LVF tivermos em mente).

\begin{factoidboxe}Introduzir uma assunção é correto%Introducing an assumption is rule-sound.
\end{factoidboxe}

%If $\meta{A}$ is introduced as an assumption on line $n$, then $\meta{A}$ is among $\Delta_n$, and so $\Delta_n \entails \meta{A}$.
Se $\meta{A}$ é introduzida como uma assunção na linha $n$, então $\meta{A}$ está entre $\Delta_n$, and so $\Delta_n \entails \meta{A}$.

\begin{factoidboxe}A regra $\eand$I é correta. %$\eand$I is rule-sound.
\end{factoidboxe}

%\emph{Proof.} Consider any application of $\eand$I in any TFL-proof, i.e., something like:
\emph{Prova.} Considere qualquer aplicação de $\eand$I em qualquer prova da LVF, i.e., algo como:
\begin{proof}
	\have[i]{a}{\meta{A}}
	\have[j]{b}{\meta{B}}
	\have[n]{c}{\meta{A}\eand\meta{B}} \ai{a, b}
\end{proof}\noindent
%To show that $\eand$I is rule-sound, we assume that every line before line $n$ is shiny; and we aim to show that line $n$ is shiny, i.e.\ that $\Delta_n \entails \meta{A} \eand \meta{B}$. 
Para mostrar que $\eand$I é correto, assumimos que toda linha antes da linha $n$ é brilhante; e desejamos mostrar que a linha $n$ é brilhante, i.e.\ que $\Delta_n \entails \meta{A} \eand \meta{B}$. 

%So, let $v$ be any valuation that makes all of $\Delta_{n}$ true. 
Então, seja $v$ qualquer avaliação que torne todas as fórmulas de $\Delta_{n}$ verdadeiras.

%We first show that $v$ makes $\meta{A}$ true. To prove this, note that all of $\Delta_i$ are among $\Delta_{n}$. By hypothesis, line $i$ is shiny. So any valuation that makes all of $\Delta_i$ true makes $\meta{A}$ true. Since $v$ makes all of $\Delta_i$ true, it makes $\meta{A}$ true too.
Primeiro mostramos que $v$ torna $\meta{A}$ verdadeiro. Para provar isso, note que todas as fórmulas de $\Delta_i$ estão entre $\Delta_{n}$. Por hipótese, a linha $i$ é brilhante. Então, qualquer valoração que torne todos de $\Delta_i$ verdadeiros torna $\meta{A}$ verdadeiro. Uma vez que $v$ torna todos de $\Delta_i$ verdadeiros, ele torna $\meta{A}$ verdadeiros também.

%We can similarly see that $v$ makes $\meta{B}$ true. 
Podemos, de maneira similar, ver que $v$ torna $\meta{B}$ verdadeiro.

%So $v$ makes $\meta{A}$ true and $v$ makes $\meta{B}$ true. Consequently, $v$ makes $\meta{A}\eand\meta{B}$ true. So any valuation that makes all of the sentences among $\Delta_{n}$ true also makes $\meta{A} \eand \meta{B}$ true. That is: line $n$ is shiny. QED

Então, $v$ torna $\meta{A}$ verdadeiro e $v$ torna $\meta{B}$ verdadeiro. Consequentemente, $v$ torna $\meta{A}\eand\meta{B}$ verdadeiro. Então, qualquer valoração que torna todas as sentenças entre $\Delta_{n}$ verdadeiras também torna $\meta{A} \eand \meta{B}$ verdadeiro. Ou seja: a linha $n$ é brilhante. QED


%All of the remaining lemmas establishing rule-soundness will have, essentially, the same structure as this one did.
Todos os lemas restantes que estabelecem a correção de regras terão essencialmente a mesma estrutura que este. 

%\begin{factoidboxe}$\eand$E is rule-sound.
\begin{factoidboxe}A regra $\eand$E é correta.
\end{factoidboxe}

%\emph{Proof.}
\emph{Prova.}
	%Assume that every line before line $n$ on some TFL-proof is shiny, and that $\eand$E is used on line $n$. So the situation is:
	Assuma que toda linha antes da linha $n$ em alguma prova da LVF é brilhante, e que $\eand$E é usada na linha $n$. Então, a situação é:
		   \begin{proof}
			   \have[i]{ab}{\meta{A}\eand\meta{B}}
			   \have[n]{a}{\meta{A}} \ae{ab}
		   \end{proof}\noindent
%(or perhaps with $\meta{B}$ on line $n$ instead; but similar reasoning will apply in that case). Let $v$ be any valuation that makes all of $\Delta_{n}$ true. Note that all of $\Delta_i$ are among $\Delta_{n}$. By hypothesis, line $i$ is shiny. So any valuation that makes all of $\Delta_i$ true makes $\meta{A}\eand\meta{B}$ true. So $v$ makes $\meta{A}\eand\meta{B}$ true, and hence makes $\meta{A}$ true. So $\Delta_{n} \entails \meta{A}$. QED
(ou talvez com $\meta{B}$ na linha $n$; mas, um raciocínio similar se aplicará nesse caso). Seja $v$ qualquer valoração que torna todas as sentenças de $\Delta_{n}$ verdadeiras. Note que todas as sentenças de $\Delta_i$ estão entre $\Delta_{n}$. Por hipótese, a linha $i$ é brilhante. Então, qualquer valoração que torna todas as sentenças de $\Delta_i$ verdadeiras torna $\meta{A}\eand\meta{B}$ verdadeira. Então, $v$ torna $\meta{A}\eand\meta{B}$ verdadeira, e consequentemente torna $\meta{A}$ verdadeira. Então, $\Delta_{n} \entails \meta{A}$. QED


\begin{factoidboxe}A regra $\eor$I é correta.%$\eor$I is rule-sound.
\end{factoidboxe}

%We leave this as an exercise.
Deixamos este como um exercício.

\begin{factoidboxe}A regra $\eor$E é correta.%$\eor$E is rule-sound.
\end{factoidboxe}

%\emph{Proof.}
\emph{Prova.}
	%Assume that every line before line $n$ on some TFL-proof is shiny, and that $\eand$E is used on line $n$. So the situation is:
	Assuma que toda linha antes da linha $n$ em alguma prova da LVF é brilhante, e que $\eand$E é usada na linha $n$. Então, a situação é:
   \begin{proof}
	   \have[m]{aob}{\meta{A}\eor\meta{B}}
	   \open
		   \hypo[i]{a}{\meta{A}} %\by{want \meta{C}}{}
		   \have[j]{c1}{\meta{C}}
	   \close
	   \open
		   \hypo[k]{b}{\meta{B}} %\by{want \meta{C}}{}
		   \have[l]{c2}{\meta{C}}
	   \close
	   \have[n]{ab}{\meta{C}}\oe{aob, a-c1,b-c2}
   \end{proof}\noindent
%Let $v$ be any valuation that makes all of $\Delta_{n}$ true. Note that all of $\Delta_m$ are among $\Delta_{n}$. By hypothesis, line $m$ is shiny. So any valuation that makes $\Delta_{n}$ true makes $\meta{A} \eor \meta{B}$ true. So in particular, $v$ makes $\meta{A} \eor \meta{B}$ true, and hence either $v$ makes $\meta{A}$ true, or $v$ makes $\meta{B}$ true. We now reason through these two cases:
Seja $v$ qualquer valoração que torna todas as sentenças de $\Delta_{n}$ verdadeiras. Note que todas as sentenças de $\Delta_m$ estão entre $\Delta_{n}$. Por hipótese, a linha $m$ é brilhante. Então, qualquer valoração que torna $\Delta_{n}$ verdadeira torna $\meta{A} \eor \meta{B}$ verdadeira. Então, em particular, $v$ torna $\meta{A} \eor \meta{B}$ verdadeira, e, consequentemente, ou $v$ torna $\meta{A}$ verdadeira, ou $v$ torna $\meta{B}$ verdadeira. Nós agora raciocinamos por entre estes dois casos:
   \begin{ebullet}
	   %\item[\emph{Case 1: $v$ makes $\meta{A}$ true.}] All of $\Delta_i$ are among $\Delta_{n}$, with the possible exception of $\meta{A}$. Since $v$ makes all of $\Delta_{n}$ true, and also makes $\meta{A}$ true,  $v$ makes all of $\Delta_i$ true. Now, by assumption, line $j$ is shiny; so $\Delta_{j} \entails \meta{C}$. But the sentences $\Delta_i$ are just the sentences $\Delta_{j}$, so $\Delta_i \entails \meta{C}$. So, any valuation that makes all of $\Delta_i$ true makes $\meta{C}$ true. But $v$ is just such a valuation. So $v$ makes $\meta{C}$ true. 
	   %
	   \item[\emph{Caso 1: $v$ torna $\meta{A}$ verdadeira.}] Todas as sentenças de $\Delta_i$ estão entre $\Delta_{n}$, com a possível exceção de $\meta{A}$. Uma vez que $v$ torna todas de $\Delta_{n}$ verdadeiras, e também torna $\meta{A}$ verdadeira,  $v$ torna todas de $\Delta_i$ verdadeiras. Agora, por hipótese, linha $j$ é brilhante; então, $\Delta_{j} \entails \meta{C}$. Mas as sentenças $\Delta_i$ são exatamente as sentenças $\Delta_{j}$, então, $\Delta_i \entails \meta{C}$. Então, qualquer valoração que torna todas as sentenças de $\Delta_i$ verdadeiras torna $\meta{C}$ verdadeira. Mas $v$ é uma tal valoração. Então, $v$ torna $\meta{C}$ verdadeira. 
	   
	  % \item[\emph{Case 2: $v$ makes $\meta{B}$ true.}] Reasoning in exactly the same way, considering lines $k$ and $l$, $v$ makes $\meta{C}$ true.
	   \item[\emph{Caso 2: $v$ torna $\meta{B}$ verdadeira.}] Raciocinar da exata mesma maneira, considerando as linhas $k$ e $l$, $k$ torna $\meta{c}$ verdadeira.
	   \end{ebullet}
%Either way, $v$ makes $\meta{C}$ true. So $\Delta_n \entails \meta{C}$.
De qualquer maneira, $v$ torna $\meta{C}$ verdadeira. Então, $\Delta_n \entails \meta{C}$.
QED


\begin{factoidboxe}
	%$\enot$E is rule-sound.
	A regra $\enot$E correta.
\end{factoidboxe}

\emph{Prova. }%\emph{Proof.}
	%Assume that every line before line $n$ on some TFL-proof is shiny, and that $\enot$E is used on line $n$. So the situation is:
	Assuma que cada linha antes da linha $n$ em alguma prova da LVF é brilhante, e que $\enot$E é usada na linha $n$. Então, a situação é:
\begin{proof}
   \have[i]{i}{\meta{A}} 
   \have[j]{j}{\enot\meta{A}}
   \have[n]{nb}{\ered}\ri{i, j}
\end{proof}\noindent
%Note that all of $\Delta_i$ and all of $\Delta_j$ are among $\Delta_{n}$. By hypothesis, lines $i$ and $j$ are shiny. So any valuation which makes all of $\Delta_{n}$ true would have to make both $\meta{A}$ and $\enot\meta{A}$ true. But no valuation can do that. So no valuation makes all of $\Delta_{n}$ true. So $\Delta_{n} \entails \ered$, vacuously.
Note que todas as sentenças de $\Delta_i$ e todas as de $\Delta_j$ estão entre $\Delta_{n}$. Então, qualquer valoração que torne verdadeiras todas as sentenças de $\Delta_{n}$ também teria que tornar tanto $\meta{A}$ quanto $\enot\meta{A}$ verdadeiras. Mas, nenhuma valoração pode fazer isso. Então, nenhuma valoração torna verdadeiras todas as sentenças de $\Delta_{n}$. Então, $\Delta_{n} \entails \ered$, vacuosamente.
QED

\begin{factoidboxe}
	%X is rule-sound.
	A regra X é correta.
\end{factoidboxe}

%We leave this as an exercise.
Deixamos esta como um exercício.

\begin{factoidboxe}
	A regra $\enot$I é correta.%$\enot$I is rule-sound.
\end{factoidboxe}

\emph{Prova.}%\emph{Proof.}
	%Assume that every line before line $n$ on some TFL-proof is shiny, and that $\enot$I is used on line $n$. So the situation is:
	Assuma que toda linha antes da linha $n$ de alguma prova da LVF é brilhante, e que $\enot$I é usada na linha $n$. Então, a situação é:
\begin{proof}
   \open
	   \hypo[i]{a}{\meta{A}}
	   \have[j]{b}{\ered}
   \close
   \have[n]{na}{\enot\meta{A}}\ni{a-b}
\end{proof}\noindent
%Let $v$ be any valuation that makes all of $\Delta_{n}$ true. Note that all of $\Delta_{n}$ are among $\Delta_i$, with the possible exception of $\meta{A}$ itself. By hypothesis, line $j$ is shiny. But no valuation can make `$\ered$' true, so no valuation can make all of $\Delta_{j}$ true. Since the sentences $\Delta_i$ are just the sentences $\Delta_{j}$, no valuation can make all of $\Delta_i$ true. Since $v$ makes all of $\Delta_{n}$ true, it must therefore make $\meta{A}$ false, and so make $\enot \meta{A}$ true. So $\Delta_n \entails \enot \meta{A}$.
Seja $v$ qualquer valoração que torne verdadeiras todas as sentenças de $\Delta_{n}$. Note que todas as sentenças de $\Delta_{n}$ estão entre $\Delta_i$, com a possível exceção de $\meta{A}$. Por hipótese, a linha $j$ é brilhante. Mas, nenhuma valoração pode tornar `$\ered$' verdadeira, então, nenhuma valoração pode tornar todas as sentenças de $\Delta_{j}$ verdadeiras. Uma vez que as sentenças $\Delta_i$ são exatamente as sentenças $\Delta_{j}$, nenhuma valoração pode tornar todas de $\Delta_i$ verdadeiras. Uma vez que $v$ torna todas de $\Delta_{n}$ verdadeiras, ela deve, portanto, tornar $\meta{A}$ falsa, e, então, tornar $\enot \meta{A}$ verdadeira. Então, So $\Delta_n \entails \enot \meta{A}$.
QED


%\begin{factoidboxe}\label{lem:LastRuleSound} IP, $\eif$I,  $\eif$E, $\eiff$I, and $\eiff$E are all rule-sound.
\begin{factoidboxe}\label{lem:LastRuleSound} As regras IP, $\eif$I,  $\eif$E, $\eiff$I, e $\eiff$E são todas corretas.
\end{factoidboxe}

Deixamos este como exercício.%We leave these as exercises.

%This establishes that all the basic rules of our proof system are rule-sound. Finally, we show:
Isso estabelece que todas as regras básicas do nosso sistema de prova são corretas. Finalmente, mostramos:

%\begin{factoidboxe}All of the derived rules of our proof system are rule-sound.
\begin{factoidboxe}Todas as regras derivadas do nosso sistema são completas.
\end{factoidboxe}

\emph{Prova.}
	%Suppose that we used a derived rule to obtain some sentence, $\meta{A}$, on line $n$ of some TFL-proof, and that every earlier line is shiny. Every use of a derived rule can be replaced (at the cost of long-windedness) with multiple uses of basic rules. That is to say, we could have used basic rules to write $\meta{A}$ on some line $n + k$, without introducing any further assumptions. So, applying our individual results that all basic rules are rule-sound several times ($k + 1$ times, in fact), we can see that line $n+k$ is shiny. Hence the derived rule is rule-sound. 
	Suponha que usamos uma regra derivada para obter alguma sentença, $\meta{A}$, na linha $n$ de alguma prova da LVF, e que toda linha anterior é brilhante. Todo uso de uma regra derivada pode ser substituído (aos custos da longevidade) por múltiplos usos das regras básicas. Isto é, poderíamos ter usado as regras básicas para escrever $\meta{A}$ em alguma linha $n + k$, sem introduzir qualquer outra assunção. Então, ao aplicar várias vezes nossos resultados individuais de que todas as regras básicas são corretas ($k + l$ vezes, na verdade), podemos ver que a linha $n+k$ é brilhante. Consequentemente, a regra derivada é correta.
QED
	

%And that's that! We have shown that every rule---basic or otherwise---is rule-sound, which is all that we required to establish the Shininess Lemma, and hence the Soundness Theorem.
E é isso! Nós mostramos que todas as regras---básicas ou não---são corretas, que é tudo o que precisávamos para estabelecer o Lema do Brilho, e, consequentemente, o Teorema da Correção.

%But it might help to round off this chapter if we repeat my informal explanation of what we have done. A formal proof is just a sequence---of arbitrary length---of applications of rules. We have shown that any application of any rule will not lead you astray. It follows (by induction)that no formal proof will lead you astray. That is: our proof system is sound. 

Mas, pode ajudar a terminar este capítulo se repetirmos minha explicação informal do que nós fizemos. Uma prova formal é apenas uma sequência---de tamanho arbitrário---de aplicações de regras. Mostramos que qualquer aplicação de qualquer regra não nos levará a enganos. Segue-se (por indução) que nenhuma prova formal nos levará a enganos. Ou seja: nosso sistema de prova é correto.

\practiceproblems

\problempart
\label{pr.Soundness}
%Complete the Lemmas left as exercises in this chapter. That is, show that the following are rule-sound:
Complete os lemas deixados como exercício neste capítulo. Ou seja, mostre que as seguintes regras são corretas:
	\begin{earg}
		%\item $\eor$I. (\emph{Hint}: this is  similar to the case of $\eand$E.)
		%\item X. (\emph{Hint}: this is similar to the case of $\enot$E.)
		%\item $\eif$I. (\emph{Hint}: this is similar to $\eor$E.)
		%\item $\eif$E.
		%\item IP. (\emph{Hint}: this is similar to the case of $\enot$I.)
		%
		\item $\eor$I. (\emph{Dica}: este caso é similar ao caso de $\eand$E.)
		\item X. (\emph{Dica}: este caso é similar ao caso de $\enot$E.)
		\item $\eif$I. (\emph{Dica}: este caso é similar ao caso de $\eor$E.)
		\item $\eif$E.
		\item IP. (\emph{Dica}: este caso é similar ao caso de $\enot$I.)
	\end{earg}

